Nuprl Lemma : box!_wf
11,40
postcript
pdf
B
:Type,
P
:(
B
). []!
P
(
B
Type)
latex
Definitions
P
Q
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
[]!
P
,
t
T
,
,
x
:
A
.
B
(
x
)
origin
B:Type, P:(B
). []!P 
(BType) B:Type, P:(B). []!P (BType) 
Q
x:A. B(x) Tx:A. B(x)